b:. (b)  (b = tt) 

latex

ProofTree

Definitions	t  T, P  Q, x:A. B(x), Unit, , False, A, , ff, , tt
Lemmas	bool wf, assert wf, btrue wf, assert of ff